Termination Proof Script

• Consider the SCC {26}. There are no usable rules. By taking the AF π with π(ADD) = 1 together with the lexicographic path order with empty precedence, rule 26 is strictly decreasing.


• Consider the SCC {24}. There are no usable rules. By taking the AF π with π(DBL) = 1 together with the lexicographic path order with empty precedence, rule 24 is strictly decreasing.


• Consider the SCC {20}. There are no usable rules. By taking the AF π with π(SQR) = 1 together with the lexicographic path order with empty precedence, rule 20 is strictly decreasing.


• Consider the SCC {27,29,31-34}. By taking the AF π with π(activate) = π(ACTIVATE) = π(dbl) = π(n__s) = π(n__terms) = π(s) = π(sqr) = π(terms) = 1 and π(add) = π(cons) = π(FIRST) = 2 together with the lexicographic path order with precedence 0 ≻ nil and n__first ≈ first, the rules in {1-7,9-16,27,29,31} are weakly decreasing and the rules in {8,32-34} are strictly decreasing. There is one new SCC.
  • Consider the SCC {29,31}. There are no usable rules. By taking the AF π with π(ACTIVATE) = π(n__s) = 1 together with the lexicographic path order with empty precedence, rule 31 is weakly decreasing and rule 29 is strictly decreasing. There is one new SCC.
    • Consider the SCC {31}. By taking the AF π with π(ACTIVATE) = 1 together with the lexicographic path order with empty precedence, rule 31 is strictly decreasing.